Nuprl Definition : inject 12,41
basic
Inj(A;B;f) == a1, a2:A. (f(a1) = f(a2))  (a1 = a2) 
latex

clarification:

basic
Inj(A;B;f) == a1:A, a2:A. (f(a1) = f(a2)  B)  (a1 = a2  A) 
latex

Definitionsx:A. B(x), P  Q, f(a), s = t
FDL editor aliasesinject

origin